#include "PDTNumVar.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"
#include "PDTType.h"

PDTNumVar::PDTNumVar(PDTCodeGraph & CG, string name, PDTQuantifier * aq, PDTIntRange * aRange) :
  PDTExpNumSing(CG), PDTVar(name, aq, aRange)
{
  CG.addVar(this);
  cloneID = 0;
  if (aRange != NULL) {
      PDTNode * node = this->getNode();
      node->addChild(aRange);
      aRange->addParent(this);
  }
}

Z3_ast
PDTNumVar::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  if (Z3node != NULL)
    return Z3node;
/*
  this->numID++;
  string temp = "n";
  temp = temp.append(inttochar(this->numID));
  const char * name = temp.c_str();
*/
  char * name = makeUniqueName(getName().c_str());
  Z3_symbol sym = Z3_mk_string_symbol(ZV.ctx, name);
  Z3node = Z3_mk_const(ZV.ctx, sym, ZV.Var);

  return Z3node;
}

Z3_ast
PDTNumVar::Z3value(PDTZ3Visitor &ZV)
{
    Z3_ast val = ZV.mk_binary_app(ZV.ctx, ZV.Vs2i, Z3node, ZV.current);
    return val;
}
